c formula generated with seed 2, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.410000
c the planted solution is {1, 3, 6, 7, 9, 10, 11, 14, 16, 17, 19, 20, 23, 24, 25, 30, 32, 33, 34, 35, 38, 41, 43, 44, 48, 49, 50, 52, 53, 55, 56, 58, 59, 61, 62, 63, 66, 70, 71, 72, 74, 75, 80, 84, 92, 93, 95, 96, 98, 99, 100, 101, 106, 108, 111, 112, 117, 118, 119, 123, 124, 125, 126, 128, 129, 132, 134, 136, 137, 138, 140, 141, 143, 145, 146, 147, 148, 150, 151, 152, 154, 155, 156, 161, 162, 165, 166, 168, 169, 170, 171, 172, 173, 176, 177, 178, 182, 183, 184, 186, 187, 189, 191, 192, 193, 196, 198, 201, 202, 203, 204, 205, 210, 211, 212, 213, 216, 218, 221, 223, 225, 229, 231, 232, 233, 234, 236, 238, 239, 240, 242, 244, 245, 247, 248, 251, 252, 253, 254, 256, 259, 260, 263, 265, 269, 270, 274, 279, 280, 286, 288, 290, 291, 292, 293, 294, 297, 298, 299, 306, 308, 309, 310, 312, 314, 315, 316, 317, 321, 322, 325, 326, 334, 336, 343, 344, 345, 354, 357, 364, 367, 370, 372, 373, 376, 378, 379, 380, 381, 383, 385, 387, 388, 390, 391, 397}
p cnf 400 1764
-209 -216 164 0
313 390 323 0
-322 399 292 0
290 -36 193 0
-265 48 -126 0
104 13 -158 0
-329 -147 -387 0
66 -246 -360 0
-370 367 -372 0
71 138 -197 0
-184 -139 185 0
-257 -126 104 0
-275 321 -261 0
142 313 -5 0
232 9 -392 0
274 149 81 0
379 251 -332 0
153 -157 -203 0
380 266 -344 0
-60 145 247 0
398 -94 -118 0
360 397 -245 0
264 78 210 0
-57 117 -266 0
-374 39 40 0
-125 -388 -144 0
242 296 -303 0
-387 247 -161 0
-223 376 -229 0
113 255 -130 0
-85 -212 -370 0
-347 -122 191 0
-87 190 303 0
64 -160 -378 0
-109 -351 118 0
-212 323 260 0
26 -327 369 0
-292 -133 -317 0
-398 296 -154 0
400 -61 211 0
60 -305 262 0
145 364 101 0
228 351 -249 0
-138 185 357 0
128 248 -361 0
140 -267 38 0
381 183 -396 0
-163 -244 250 0
142 -134 136 0
-197 12 81 0
395 122 248 0
-278 -309 -118 0
113 212 -231 0
-49 -63 -258 0
-272 157 289 0
42 86 -276 0
383 315 203 0
363 364 94 0
-350 -367 -210 0
322 43 63 0
-291 368 -267 0
266 -151 280 0
-20 377 225 0
153 227 -392 0
360 -294 -318 0
-13 -193 346 0
270 -393 -167 0
-110 -397 226 0
116 -317 -300 0
-306 93 130 0
-131 74 370 0
2 144 -289 0
240 114 200 0
119 306 -197 0
-384 110 31 0
126 -50 67 0
-321 85 72 0
150 -152 -124 0
43 17 -361 0
238 -350 260 0
-305 -303 1 0
178 -224 -305 0
-313 -52 -306 0
-354 367 394 0
-261 -184 -212 0
-134 10 -126 0
-332 189 201 0
329 -9 -85 0
253 -53 352 0
23 143 -377 0
48 397 -277 0
-16 382 63 0
-235 -79 -271 0
156 237 -357 0
334 173 -318 0
-170 -135 272 0
140 -54 -300 0
252 -306 -265 0
-130 352 -279 0
331 162 267 0
132 -365 80 0
-360 -234 370 0
386 -225 -21 0
-263 82 151 0
157 210 369 0
294 273 -148 0
76 287 -305 0
-155 -45 -391 0
258 30 -186 0
319 278 71 0
52 102 88 0
-145 -172 148 0
-281 -24 64 0
-165 68 43 0
96 111 -181 0
120 -250 -43 0
94 29 196 0
-2 -263 241 0
-220 -347 -340 0
113 181 -305 0
279 -340 -81 0
-40 97 -96 0
352 305 -83 0
173 -304 11 0
346 88 -113 0
-171 146 -251 0
230 264 44 0
-66 348 -284 0
139 -240 -368 0
29 -50 251 0
363 -359 332 0
391 334 -305 0
-265 -152 -400 0
-54 -243 -350 0
-185 -396 -102 0
-331 96 -31 0
-5 240 -361 0
241 167 -358 0
119 137 -144 0
148 284 77 0
-227 -184 235 0
69 233 2 0
-148 -373 -27 0
181 -118 106 0
-22 -373 -43 0
-233 -390 -91 0
216 -283 -285 0
-80 -218 -110 0
110 111 -171 0
-385 -218 379 0
296 121 -241 0
-395 -210 -63 0
-13 -212 -147 0
277 42 25 0
-379 -359 -245 0
78 44 -33 0
-97 -326 289 0
-342 392 127 0
-368 169 -5 0
-2 -171 158 0
-159 -333 -305 0
-170 -45 -106 0
-167 35 -285 0
-248 146 375 0
264 340 213 0
104 71 -298 0
-175 -394 325 0
333 -80 312 0
-7 11 -177 0
151 349 94 0
136 115 105 0
208 -213 -40 0
-96 -30 187 0
270 -315 -167 0
286 384 -174 0
269 212 -275 0
-289 -49 -101 0
-353 159 31 0
184 -236 -270 0
-221 285 -319 0
227 -110 -370 0
-119 304 -107 0
-182 -104 -263 0
-291 151 78 0
-150 92 -196 0
-291 118 241 0
-131 150 -45 0
187 40 107 0
-262 146 -122 0
322 246 28 0
322 -126 -136 0
345 -45 -200 0
-79 -178 -125 0
-81 -359 -76 0
-7 -175 -197 0
-168 -253 -130 0
27 384 147 0
345 -110 385 0
-337 221 202 0
284 71 -141 0
107 -217 382 0
-306 -243 166 0
-338 -257 195 0
-136 -263 62 0
-2 -289 -342 0
-135 381 170 0
-378 201 -191 0
368 148 -183 0
33 239 -153 0
-216 -191 -264 0
272 231 -125 0
-295 245 367 0
249 -285 -280 0
148 93 -386 0
354 -190 -122 0
289 200 123 0
297 243 302 0
-34 7 -44 0
302 213 -210 0
-40 -271 -289 0
-233 -97 -101 0
98 -356 -29 0
-368 106 177 0
206 -187 -362 0
85 234 114 0
-99 141 31 0
-265 -75 -5 0
355 -314 343 0
260 318 -48 0
-226 -244 230 0
246 147 -38 0
-159 303 73 0
140 40 2 0
219 -358 4 0
33 -179 344 0
-351 -314 12 0
-329 259 -12 0
-329 111 -149 0
205 -324 -5 0
101 -106 -193 0
-34 -179 -357 0
41 363 -388 0
64 -275 396 0
122 -254 -320 0
264 278 -296 0
-348 243 -48 0
-279 303 -368 0
-348 -164 -250 0
151 255 106 0
-156 231 -145 0
-255 359 83 0
-349 268 -297 0
177 -306 79 0
290 132 -323 0
-153 -384 -356 0
-97 330 -80 0
-287 38 -358 0
396 47 161 0
157 266 -304 0
191 -214 95 0
-85 122 169 0
-82 -26 294 0
228 -304 -236 0
202 203 -328 0
185 38 -193 0
213 -323 -67 0
249 369 204 0
-41 -87 157 0
85 86 -368 0
52 380 -355 0
-218 7 -101 0
-78 -97 -324 0
-14 -316 32 0
293 -359 123 0
62 -169 195 0
-75 -399 -62 0
-306 -300 -136 0
31 312 15 0
-381 -20 236 0
139 -269 -217 0
169 -272 314 0
170 -306 -234 0
-331 -149 -356 0
320 172 -290 0
277 -82 57 0
-104 54 158 0
200 -68 -344 0
-168 -170 -366 0
139 -295 2 0
284 221 -162 0
-86 -309 60 0
248 320 -223 0
137 -344 374 0
124 -103 170 0
-248 -157 93 0
188 84 122 0
84 -250 -356 0
-268 152 -65 0
-261 -240 222 0
39 -88 -145 0
-269 -52 -324 0
243 247 -172 0
-134 153 -83 0
279 -371 162 0
-373 35 -216 0
-230 271 18 0
-290 -378 -39 0
-241 -272 192 0
-143 348 205 0
-259 198 -242 0
-187 79 111 0
163 400 242 0
234 326 -396 0
322 -249 245 0
208 49 77 0
239 194 -367 0
342 47 -144 0
-45 -356 -377 0
249 396 -393 0
307 -383 232 0
155 -165 240 0
113 232 -211 0
-295 -100 164 0
339 -303 386 0
-314 -50 96 0
-352 -273 -142 0
-347 131 144 0
-174 -259 287 0
127 27 -273 0
-333 -155 -55 0
97 -270 52 0
-208 -383 -279 0
-38 24 362 0
115 -171 317 0
-155 245 142 0
90 179 321 0
-213 193 -232 0
86 316 89 0
-62 128 110 0
-187 25 -117 0
-174 -240 313 0
-392 223 41 0
-66 -165 -264 0
-369 -287 232 0
51 -382 -128 0
216 100 -194 0
-78 54 88 0
-327 -13 -45 0
-54 78 133 0
-92 -262 -145 0
-80 -31 349 0
-168 97 165 0
-354 -301 -252 0
-7 -349 55 0
177 -263 195 0
-18 383 151 0
208 -400 -274 0
-87 -256 -253 0
268 -374 -9 0
287 400 -361 0
-195 -268 50 0
267 -274 155 0
-13 243 368 0
124 -147 -152 0
-178 -380 294 0
368 -178 119 0
-375 292 -157 0
110 -226 -58 0
-80 -388 35 0
306 52 298 0
-330 345 95 0
-333 229 -325 0
-388 -349 27 0
-395 43 -369 0
-138 393 96 0
233 388 156 0
293 -320 41 0
43 156 274 0
37 323 380 0
-48 376 -354 0
-89 249 152 0
379 76 -299 0
-235 303 -326 0
185 -305 -151 0
387 109 246 0
-124 -117 119 0
228 -291 -355 0
271 124 167 0
105 -127 356 0
-209 43 -18 0
-99 -42 329 0
-351 -127 -209 0
-310 -176 -97 0
-281 -368 -382 0
-313 -277 349 0
-78 -285 -104 0
-57 145 -107 0
-175 -316 -297 0
-47 -178 27 0
-223 151 -34 0
30 -334 394 0
-126 257 -377 0
-278 222 13 0
295 -339 235 0
-385 380 185 0
148 233 -394 0
126 -363 236 0
-283 224 -92 0
-40 371 -364 0
40 -28 160 0
-221 277 -262 0
-369 -379 271 0
-167 25 375 0
-143 52 88 0
-267 254 334 0
225 -288 -150 0
286 261 -238 0
-262 -153 285 0
-120 211 -301 0
-194 -397 -161 0
78 14 98 0
-315 208 325 0
224 -232 162 0
-212 -20 -273 0
-46 254 -243 0
85 247 275 0
67 233 -178 0
372 -176 -123 0
263 74 344 0
216 303 81 0
372 -25 -391 0
296 -202 -278 0
59 -301 -333 0
-170 -7 34 0
-46 143 -28 0
-33 386 -167 0
-200 -14 -165 0
227 -189 147 0
386 289 292 0
-192 -300 83 0
35 -22 -337 0
-95 180 -26 0
-285 -342 -318 0
266 207 24 0
-15 -120 357 0
-1 -158 -240 0
-73 67 -20 0
-301 -340 -30 0
221 -379 102 0
-233 144 112 0
-60 -48 368 0
-306 -178 -352 0
-330 -398 -73 0
-115 119 -102 0
164 291 12 0
-130 -241 56 0
293 -137 261 0
-216 65 -352 0
211 257 103 0
-328 185 22 0
-249 260 387 0
172 -252 -17 0
-143 -368 320 0
-132 -26 243 0
-358 -218 -43 0
39 -40 -74 0
243 -390 -296 0
151 -130 -349 0
-215 354 -304 0
-84 -257 -74 0
-106 -12 -149 0
-376 200 -18 0
2 150 -138 0
298 -188 169 0
80 228 335 0
-260 -74 -281 0
-210 -38 -338 0
-67 -70 393 0
-90 -199 -83 0
-33 -2 107 0
219 72 319 0
69 -215 54 0
-367 -162 -349 0
283 14 207 0
-303 236 -116 0
137 -222 376 0
63 3 -116 0
-242 239 384 0
199 98 -129 0
-275 -46 310 0
230 59 337 0
213 -129 2 0
-319 -220 -110 0
366 333 -356 0
106 -185 7 0
-288 -4 272 0
9 -354 -270 0
266 179 310 0
-242 84 177 0
308 -350 96 0
272 333 385 0
362 -247 254 0
-134 -269 229 0
204 112 -92 0
124 368 375 0
264 -377 375 0
395 -74 -324 0
-353 -307 -227 0
242 -28 -399 0
41 218 -26 0
-56 383 228 0
-162 281 -87 0
321 -27 -18 0
-271 -343 318 0
384 185 -69 0
-398 -61 -259 0
345 -12 -175 0
-398 155 40 0
114 352 156 0
217 181 210 0
216 -400 -339 0
369 359 306 0
-27 229 366 0
165 300 -351 0
-120 394 257 0
201 -220 321 0
-252 -245 96 0
309 -278 -266 0
-346 195 113 0
-400 -49 -393 0
-172 390 -398 0
145 -106 393 0
346 -11 -363 0
-290 -291 -327 0
-151 -211 -22 0
-10 387 395 0
5 134 262 0
-144 -313 182 0
-208 175 -279 0
-169 -324 -223 0
-260 -142 137 0
372 -121 247 0
-44 124 -269 0
150 236 50 0
5 60 150 0
-76 11 72 0
34 -143 -191 0
32 -213 -231 0
285 -363 -378 0
313 129 -204 0
-385 122 265 0
279 -264 -349 0
-241 -42 -14 0
-397 -202 -65 0
-105 -211 69 0
69 -71 124 0
-33 -61 -153 0
20 -239 333 0
-19 -196 55 0
152 -82 321 0
-356 125 270 0
-363 -331 -40 0
-373 29 334 0
-290 -193 -215 0
-146 185 344 0
335 206 92 0
-243 203 -2 0
125 -351 -199 0
100 106 -272 0
318 393 244 0
357 -254 266 0
259 385 242 0
255 -318 -136 0
176 396 219 0
-95 336 4 0
211 115 -387 0
-383 -183 136 0
390 103 295 0
331 -269 225 0
300 -5 -274 0
158 -20 -21 0
-94 -107 171 0
361 336 345 0
-278 298 -385 0
33 40 -193 0
-1 97 391 0
98 317 390 0
-258 124 -65 0
103 -193 385 0
-377 -99 54 0
-196 -222 13 0
-95 -58 17 0
-132 18 -188 0
-247 -60 -231 0
-336 -181 240 0
252 -71 277 0
44 -160 -195 0
-281 -62 -233 0
366 -238 -12 0
289 -161 35 0
377 114 -284 0
-381 77 59 0
-170 363 -400 0
360 -211 251 0
-371 -304 -116 0
311 -243 -172 0
-393 397 -42 0
194 167 198 0
21 284 48 0
-200 167 179 0
-49 375 252 0
-271 -354 275 0
-375 -40 227 0
145 349 -169 0
-271 157 249 0
-270 -49 93 0
-144 273 -381 0
-52 108 66 0
-172 125 -391 0
379 22 -299 0
387 -384 -163 0
221 -319 -301 0
-372 275 -285 0
-348 -357 46 0
36 284 -54 0
118 -87 166 0
-276 118 345 0
31 90 245 0
127 -136 -369 0
-198 224 -362 0
25 10 286 0
295 -269 50 0
-106 -232 292 0
-361 394 -10 0
333 291 -314 0
96 178 -241 0
-239 -392 -44 0
-299 -161 379 0
375 -128 -215 0
322 133 -61 0
189 -353 -2 0
-68 240 -343 0
-386 -229 -373 0
129 58 387 0
283 -89 305 0
-88 -72 -212 0
-331 -211 273 0
219 -382 282 0
-142 383 -68 0
49 77 374 0
-144 311 257 0
367 347 -146 0
-387 218 -162 0
190 362 259 0
-37 364 -121 0
379 -107 -275 0
17 104 -7 0
-81 -342 -267 0
-222 124 367 0
-93 4 345 0
-9 -169 -149 0
151 -185 256 0
288 146 106 0
-168 -131 209 0
-234 265 -162 0
14 -81 -384 0
20 -283 371 0
363 -308 -57 0
9 -67 -73 0
-119 144 -209 0
197 320 72 0
298 380 -371 0
-385 44 22 0
149 160 -217 0
310 -279 -33 0
-4 -271 3 0
321 384 133 0
-133 -304 -301 0
283 307 30 0
93 -258 -4 0
-185 330 -128 0
-396 -80 382 0
4 -39 31 0
188 -133 179 0
-333 -32 -269 0
-276 22 56 0
-352 -101 350 0
-48 -160 228 0
102 -97 217 0
-25 271 -333 0
-20 -228 -99 0
329 -236 385 0
242 135 330 0
216 -285 388 0
-223 205 -106 0
38 -250 -361 0
-229 -142 -52 0
71 -219 -362 0
121 102 -289 0
307 -210 286 0
342 176 -119 0
212 95 322 0
37 282 52 0
188 -240 -139 0
-231 50 -221 0
384 110 -281 0
334 172 -46 0
209 -179 -42 0
54 -299 -365 0
-44 368 293 0
74 -2 -160 0
-75 171 -325 0
-253 229 -25 0
223 -76 -277 0
-180 -380 -259 0
-239 18 -369 0
-43 202 -279 0
-316 -66 -329 0
293 174 -364 0
30 -111 105 0
-26 -85 -283 0
24 377 80 0
235 332 125 0
-268 -101 400 0
-35 -277 262 0
-194 -171 264 0
-36 224 -391 0
-60 -152 -43 0
-23 7 115 0
-47 224 89 0
392 106 -260 0
212 182 140 0
-217 322 -14 0
95 -31 129 0
-45 30 -195 0
22 -148 -230 0
232 -230 186 0
332 308 -123 0
141 -136 237 0
27 -185 -93 0
2 20 51 0
102 55 88 0
217 -257 350 0
-93 -24 -346 0
-289 230 -377 0
-46 216 -341 0
-22 -333 169 0
-218 33 -306 0
-335 188 105 0
345 -219 -179 0
-39 -75 -170 0
-293 121 70 0
-312 -21 320 0
185 94 -104 0
15 19 -83 0
-284 283 12 0
308 -300 -351 0
-208 -61 -274 0
-39 -400 260 0
-170 98 356 0
-267 -247 -286 0
-96 -56 -114 0
-119 -83 374 0
-16 -76 -154 0
-107 -224 -109 0
-305 -215 308 0
-86 -41 -373 0
400 -377 -169 0
-258 226 200 0
-4 -187 -344 0
286 237 -183 0
-277 399 175 0
127 229 103 0
-325 199 -331 0
337 -44 -160 0
42 -194 69 0
-285 166 176 0
215 174 -120 0
59 -395 -68 0
19 -287 -115 0
140 128 -127 0
-359 -102 80 0
-284 53 -321 0
-1 -135 235 0
40 -392 -200 0
-272 80 -235 0
115 325 277 0
47 -79 219 0
136 336 312 0
-5 364 -69 0
119 363 46 0
313 76 172 0
-283 -223 -53 0
65 150 114 0
201 -254 351 0
-65 -221 346 0
357 315 112 0
-119 -359 -117 0
-84 -255 -96 0
334 35 240 0
-108 -116 250 0
354 16 -2 0
289 -227 272 0
86 59 -298 0
-179 -264 336 0
-169 137 120 0
-280 51 171 0
103 -160 -156 0
-287 379 -78 0
367 124 -80 0
-303 123 -60 0
-333 73 393 0
-309 -89 -136 0
326 347 235 0
-379 -297 -87 0
-147 215 125 0
-37 -234 -58 0
-212 -149 -244 0
-164 226 -30 0
-100 229 206 0
390 -91 -396 0
-4 372 -89 0
-21 225 -396 0
-348 -56 190 0
-400 -185 372 0
236 248 317 0
-72 87 -64 0
166 351 -203 0
-320 67 -7 0
97 184 332 0
-160 -358 -102 0
-347 97 103 0
-326 9 -322 0
217 -266 -74 0
-87 85 -372 0
32 211 158 0
-285 320 -387 0
309 -181 -102 0
380 -149 -327 0
236 -320 334 0
-205 317 -336 0
128 -348 -159 0
-59 -80 184 0
-98 -294 -377 0
-154 105 -320 0
-114 -285 316 0
-389 313 -379 0
366 288 22 0
65 -342 243 0
-209 -14 273 0
-136 -315 186 0
-28 265 -86 0
-399 -72 -70 0
148 2 160 0
-142 -220 -338 0
23 -248 -232 0
279 147 309 0
-395 114 358 0
280 126 166 0
72 198 387 0
-395 380 -107 0
253 71 -398 0
196 149 21 0
246 -248 -79 0
-392 206 -32 0
-32 -311 -72 0
-185 249 366 0
299 76 -225 0
234 -356 297 0
-155 86 170 0
-324 134 274 0
193 -14 -263 0
157 210 -192 0
89 -221 -78 0
-230 -210 -270 0
40 204 167 0
-268 -243 315 0
227 38 -348 0
-269 93 -153 0
305 231 -373 0
273 311 213 0
170 60 164 0
-282 -380 85 0
-323 -369 -142 0
-240 -85 -294 0
367 107 -58 0
200 90 -159 0
-103 -52 -288 0
-146 246 -181 0
390 -271 16 0
-64 -328 -113 0
30 104 -259 0
-70 -275 330 0
-208 252 -175 0
-104 374 -252 0
-278 276 287 0
392 -373 391 0
43 373 -300 0
-96 134 27 0
-136 363 30 0
-138 398 168 0
95 36 105 0
39 -188 -211 0
-84 -357 35 0
-353 183 394 0
107 305 -361 0
64 -378 156 0
352 -154 -323 0
9 -262 -243 0
134 311 -213 0
-115 -263 -138 0
256 -264 169 0
-19 116 43 0
-83 -173 264 0
374 136 299 0
366 -134 -348 0
152 356 275 0
-256 -122 277 0
316 239 152 0
230 201 190 0
-157 146 145 0
-30 -41 -120 0
-88 -395 -104 0
-145 -195 -254 0
-224 -391 320 0
-295 -306 -62 0
310 -304 84 0
385 302 -357 0
65 -241 -390 0
34 -2 11 0
149 -34 166 0
-374 -299 -189 0
341 170 -178 0
381 -385 85 0
-306 -36 -66 0
73 272 245 0
319 209 -281 0
99 -197 55 0
173 88 304 0
187 -355 -340 0
125 242 -363 0
385 -120 256 0
-156 195 55 0
-235 309 184 0
-293 -247 -360 0
354 330 36 0
-44 143 320 0
-37 297 -288 0
-97 -342 -42 0
36 -60 115 0
-11 -209 67 0
55 -171 -234 0
-73 148 191 0
-113 134 372 0
-107 -314 37 0
194 140 -173 0
262 38 -138 0
126 -44 371 0
-256 186 -201 0
22 322 -250 0
318 216 307 0
-340 -191 -155 0
-160 -247 114 0
21 -307 -367 0
328 -16 -307 0
287 304 -67 0
280 -248 -377 0
-225 143 -260 0
-261 -179 169 0
-8 -206 -351 0
-187 364 352 0
-323 -200 -127 0
-336 -288 6 0
-166 177 112 0
-260 -270 314 0
-252 96 -119 0
-304 71 119 0
-107 6 100 0
269 137 1 0
-126 10 300 0
-204 -280 -271 0
-181 -356 -393 0
243 67 66 0
-70 -78 258 0
38 101 218 0
-204 174 -368 0
321 -40 25 0
119 -318 -79 0
-4 -271 249 0
-346 339 -140 0
-16 -362 -196 0
-281 243 174 0
-100 25 332 0
-143 -370 -350 0
345 41 -351 0
337 -238 204 0
191 -273 370 0
-344 200 299 0
-165 -195 -291 0
259 -132 -93 0
-34 377 -26 0
-346 54 -201 0
-283 -323 321 0
203 386 246 0
-67 257 250 0
4 -260 161 0
-267 -376 295 0
-387 -121 -223 0
-353 141 196 0
-129 -395 -269 0
-373 322 -334 0
253 282 -309 0
-22 -104 100 0
-125 -340 331 0
30 398 -204 0
36 395 345 0
125 -164 -393 0
-356 359 -198 0
111 255 359 0
382 355 308 0
65 205 86 0
231 169 -393 0
-64 305 -189 0
382 117 -376 0
-322 -324 164 0
129 -218 103 0
248 38 -287 0
-364 29 126 0
81 -122 304 0
-291 247 -259 0
-54 -392 -395 0
162 30 92 0
356 -4 382 0
-108 -181 114 0
32 -85 354 0
-58 -7 -305 0
299 -138 323 0
58 174 318 0
-344 315 363 0
354 -48 -72 0
-259 175 -180 0
207 -274 155 0
290 400 -298 0
-106 -17 212 0
173 -235 98 0
195 164 298 0
94 -186 370 0
54 138 10 0
-208 245 -352 0
46 -139 -334 0
-158 189 -320 0
-118 229 192 0
340 -252 41 0
-106 -382 -229 0
287 -272 351 0
-316 -284 335 0
110 -202 -284 0
382 361 173 0
128 126 -296 0
190 310 -61 0
46 316 219 0
-104 363 206 0
-146 4 138 0
233 -317 235 0
-88 138 234 0
-178 31 263 0
10 -84 5 0
-272 119 129 0
-342 49 -65 0
234 -190 -195 0
-5 -281 205 0
-23 -226 -132 0
98 -81 -271 0
77 65 234 0
-103 371 -71 0
-385 -205 -109 0
-292 130 -300 0
172 -271 20 0
280 306 229 0
-86 -113 343 0
-289 -44 -356 0
-389 -310 331 0
375 303 -241 0
-371 103 -259 0
-192 -142 243 0
393 119 399 0
-373 -103 188 0
-141 -224 168 0
219 -182 124 0
26 -209 -210 0
-209 -229 348 0
-123 -49 260 0
339 204 -108 0
145 285 -179 0
329 -22 -115 0
-289 -76 -120 0
-352 -254 261 0
107 -338 97 0
-59 366 -5 0
-370 165 88 0
-96 66 195 0
186 -311 -327 0
130 277 -36 0
396 -84 -175 0
384 -169 -214 0
-189 48 323 0
74 -186 -118 0
194 -24 -282 0
40 155 208 0
-164 141 84 0
-36 112 314 0
237 -246 341 0
-272 9 -42 0
186 381 325 0
172 56 -328 0
-380 -330 -242 0
353 -113 -254 0
91 69 146 0
206 324 80 0
280 -171 -189 0
-23 51 150 0
182 -266 -57 0
-70 -266 228 0
-370 -369 18 0
-119 -40 -367 0
-251 216 346 0
93 398 -198 0
91 -367 119 0
364 -128 396 0
-242 -205 118 0
122 -60 -269 0
-30 -7 -64 0
262 373 -344 0
31 -75 -57 0
-123 -206 -84 0
218 -336 -236 0
-59 -172 25 0
-41 84 148 0
399 136 377 0
133 -193 -278 0
-312 -133 384 0
344 -299 293 0
-261 166 -74 0
-232 -127 342 0
-10 314 22 0
209 -83 368 0
34 -187 328 0
221 -77 -230 0
-392 -368 33 0
-49 195 -222 0
43 -382 210 0
193 55 239 0
-24 159 -77 0
-293 35 240 0
-29 354 50 0
-192 205 -213 0
-74 -139 323 0
30 213 49 0
291 -333 -47 0
75 68 -274 0
308 -365 -185 0
-58 -283 15 0
-352 243 140 0
387 -13 -105 0
238 -43 -260 0
29 -192 -302 0
148 77 -299 0
250 151 -11 0
166 143 210 0
396 -193 -341 0
48 6 290 0
323 -283 76 0
-313 -234 -390 0
-300 254 -256 0
-271 -371 -197 0
303 166 -35 0
-291 -101 -159 0
139 -157 374 0
-179 -128 -314 0
-296 51 -24 0
326 -105 285 0
245 279 -200 0
287 -249 190 0
-182 -56 242 0
87 281 -296 0
-223 134 -164 0
277 -157 98 0
34 -70 391 0
-162 75 386 0
-62 -224 219 0
105 -151 232 0
145 291 117 0
278 150 341 0
-294 -273 188 0
258 -263 -220 0
-51 145 336 0
211 -203 -364 0
111 392 113 0
-28 -273 -47 0
159 25 188 0
-315 -214 -322 0
26 266 -68 0
-238 60 336 0
-302 178 388 0
-307 -123 178 0
-301 -115 298 0
125 -373 -233 0
153 -11 -175 0
119 -382 168 0
-140 -217 255 0
104 -247 -395 0
-52 -74 -167 0
-280 312 200 0
-49 69 310 0
128 134 -209 0
-167 -234 -314 0
183 145 -353 0
171 323 116 0
32 337 264 0
-397 256 39 0
106 43 -302 0
32 258 -178 0
231 316 185 0
381 157 -30 0
-285 -298 163 0
121 -86 295 0
279 -164 248 0
-344 167 -384 0
364 333 -132 0
-248 396 -267 0
-247 170 -263 0
-126 197 373 0
65 -57 257 0
29 56 330 0
-330 -87 -338 0
246 -303 -135 0
119 -39 234 0
-382 9 -42 0
-92 116 -275 0
196 -232 382 0
249 -255 -184 0
-338 78 332 0
209 -267 -238 0
-46 130 368 0
380 379 260 0
242 17 72 0
343 97 181 0
-266 68 277 0
381 -187 283 0
69 325 -124 0
-124 -296 -94 0
379 -300 99 0
172 -252 -136 0
-374 84 193 0
111 189 52 0
179 -163 97 0
-284 -359 99 0
381 397 176 0
-52 166 208 0
121 250 -18 0
-170 -266 47 0
21 207 -331 0
373 -242 241 0
-33 5 74 0
-314 -139 185 0
-55 -242 210 0
-25 319 -86 0
138 -216 209 0
-288 29 -5 0
-19 -357 -400 0
-21 -241 -268 0
-303 -226 -283 0
-91 -32 -52 0
390 287 273 0
-66 139 294 0
178 -366 95 0
23 -159 -257 0
200 371 -209 0
-125 -188 340 0
44 97 -265 0
229 67 104 0
119 -268 397 0
-228 -369 -257 0
-238 169 -253 0
-44 -177 218 0
16 -317 -33 0
-84 299 -193 0
322 69 -123 0
191 320 -338 0
-89 -287 -365 0
380 17 269 0
185 225 313 0
-175 242 187 0
243 225 -178 0
186 -368 129 0
97 76 218 0
-302 -210 -35 0
58 388 -110 0
383 -281 -64 0
-97 301 130 0
65 -46 -237 0
-134 -369 295 0
-51 -384 -237 0
-87 -271 256 0
380 -324 357 0
204 92 -361 0
106 15 -178 0
66 -38 -263 0
-63 279 340 0
19 25 -368 0
-92 365 96 0
11 -35 115 0
-343 374 -369 0
-131 -224 128 0
294 60 -65 0
339 -48 -400 0
-306 354 -93 0
205 -329 381 0
132 -113 -18 0
134 -338 158 0
-153 138 213 0
-361 128 -320 0
386 224 -149 0
121 341 -289 0
-54 -278 20 0
-65 143 70 0
359 62 123 0
-172 360 -352 0
142 -349 -14 0
-264 367 -333 0
181 -71 32 0
-107 -183 -212 0
-130 298 232 0
391 303 -38 0
397 -316 208 0
-385 -140 -67 0
-128 284 259 0
290 -255 -359 0
156 190 12 0
292 -259 219 0
280 -355 -13 0
-381 -122 -176 0
322 257 -265 0
357 -376 -258 0
208 -286 -393 0
105 -93 53 0
114 -122 219 0
387 -189 -191 0
-243 -112 -196 0
-172 -116 389 0
-157 -344 -137 0
-285 -369 143 0
11 -15 -324 0
274 -83 242 0
-80 -69 305 0
206 321 -372 0
143 -63 -265 0
-95 -178 213 0
-79 10 -28 0
-391 126 -251 0
-389 -218 -84 0
233 296 303 0
-169 -87 -397 0
375 136 86 0
-116 11 -355 0
270 -208 -76 0
258 133 -350 0
201 258 -14 0
-335 -20 257 0
-224 393 366 0
320 -222 -146 0
251 -79 232 0
276 380 -66 0
18 -196 298 0
-34 134 -294 0
-325 -7 61 0
-196 -323 -317 0
307 134 67 0
145 111 -85 0
238 -259 -23 0
-103 -341 -268 0
226 -77 105 0
-366 -39 -226 0
50 258 -35 0
-65 350 -218 0
174 309 -316 0
-75 -368 -56 0
346 -93 234 0
-92 45 198 0
47 398 203 0
169 245 -142 0
-284 -259 105 0
-115 334 63 0
23 -372 -373 0
-281 161 239 0
-263 31 166 0
326 156 -214 0
203 -387 213 0
372 20 -328 0
-222 54 -98 0
-365 -187 206 0
-22 63 -335 0
304 355 -179 0
376 348 386 0
-280 -174 51 0
-33 -313 -111 0
383 -190 136 0
-308 351 270 0
-93 207 212 0
314 367 -31 0
124 72 170 0
279 -211 42 0
148 273 -288 0
-231 315 21 0
31 -87 -173 0
-249 276 131 0
-87 -283 -31 0
385 381 -144 0
-262 135 -93 0
254 151 325 0
50 21 -41 0
-135 -148 164 0
223 106 -375 0
234 61 148 0
-383 -206 -364 0
364 -35 -19 0
18 -338 -84 0
339 -232 10 0
-22 -304 -116 0
63 254 259 0
-259 -304 -290 0
-271 -181 112 0
-180 293 155 0
-284 -301 -12 0
-239 -361 -334 0
6 -14 -112 0
40 -8 -92 0
164 257 -398 0
-242 25 -367 0
177 17 -42 0
-253 -320 398 0
94 -190 -343 0
53 -351 202 0
312 -334 -151 0
22 -227 90 0
153 -92 -68 0
184 -162 -3 0
-26 264 222 0
385 251 -301 0
-251 -363 237 0
-266 -383 342 0
283 -302 -10 0
-337 -90 -89 0
-400 293 315 0
379 -229 90 0
-129 81 34 0
332 -28 -262 0
-83 76 352 0
380 390 -230 0
142 215 -199 0
-220 327 13 0
168 -121 -179 0
18 -15 163 0
314 119 -13 0
286 190 153 0
341 190 -188 0
252 140 -398 0
198 -313 -319 0
-317 139 -235 0
166 183 -79 0
284 70 -137 0
-113 -145 -132 0
-57 -211 -172 0
18 249 -36 0
-66 -178 48 0
-72 -261 -388 0
-243 298 -307 0
170 -94 -353 0
-263 143 363 0
-249 208 21 0
206 -297 -179 0
-310 -80 390 0
10 351 174 0
-287 122 183 0
224 97 -163 0
288 -354 347 0
49 -281 176 0
-389 203 -163 0
226 -177 24 0
357 24 -258 0
214 121 -255 0
319 126 -111 0
-82 4 398 0
-131 -233 31 0
-64 -20 327 0
-109 54 -80 0
-376 162 -34 0
-315 200 -307 0
383 107 214 0
-252 52 -302 0
54 313 66 0
-370 50 396 0
-218 316 275 0
-108 -127 361 0
-97 -276 -311 0
-352 -180 390 0
340 237 165 0
-243 -353 98 0
-206 289 4 0
-342 -57 71 0
-12 -71 15 0
-76 -42 125 0
-261 -144 1 0
30 289 352 0
-91 -218 -80 0
-61 148 -100 0
243 -215 267 0
8 -120 -274 0
-375 92 146 0
93 -320 -327 0
-240 -135 -70 0
183 290 74 0
52 -315 332 0
-284 216 53 0
140 -240 341 0
161 8 302 0
-332 364 71 0
22 -2 -55 0
-79 -202 -364 0
88 362 170 0
76 233 54 0
-398 320 -269 0
283 -30 344 0
66 349 139 0
-392 -83 -37 0
-205 184 -248 0
-253 -381 -39 0
-208 8 -44 0
265 -106 130 0
-234 -108 325 0
-134 197 265 0
392 179 238 0
-319 175 -334 0
395 -174 -387 0
-119 -351 57 0
9 -22 223 0
-323 325 20 0
333 331 -271 0
169 -364 -162 0
225 224 -106 0
191 -327 -300 0
-114 137 -69 0
343 -302 -393 0
-13 -197 151 0
-106 354 102 0
-213 -330 -247 0
97 63 78 0
-388 -130 -326 0
-297 -211 -338 0
-146 -10 -337 0
177 -326 -193 0
-62 190 -130 0
-85 373 -12 0
-8 92 233 0
73 165 262 0
-163 -258 -39 0
-263 -379 -278 0
291 -77 -394 0
338 227 239 0
-278 146 345 0
334 321 -259 0
349 -388 221 0
17 59 -328 0
250 -321 -356 0
85 112 -70 0
37 73 -395 0
342 -356 369 0
-207 -34 -143 0
-396 272 -376 0
146 127 -59 0
-114 62 146 0
76 -384 -315 0
-360 -207 166 0
277 310 -176 0
124 -221 -263 0
184 -39 145 0
-338 277 -148 0
392 -10 -266 0
226 396 336 0
-398 131 -132 0
-79 47 -173 0
-131 201 178 0
-162 -17 -153 0
237 -2 257 0
11 -320 -318 0
-134 -277 -234 0
-249 -178 230 0
150 65 296 0
-257 -232 103 0
61 85 -33 0
-222 -12 30 0
240 -120 205 0
123 46 -37 0
80 -65 -282 0
200 -94 -146 0
131 -339 97 0
-21 -324 176 0
-288 124 318 0
-211 -47 149 0
-95 -298 308 0
49 271 -145 0
296 349 379 0
331 337 187 0
304 -301 399 0
357 86 207 0
144 -397 385 0
350 245 -173 0
161 337 -248 0
188 147 369 0
-265 352 252 0
83 -284 206 0
-206 -222 345 0
-390 384 -313 0
-339 353 -334 0
281 -350 -143 0
175 -328 250 0
367 -276 131 0
281 84 -231 0
341 -380 16 0
-64 -29 334 0
-332 330 295 0
-91 288 -57 0
-378 314 46 0
-280 368 -42 0
-114 134 -360 0
148 310 -115 0
-274 -310 111 0
-99 270 -346 0
130 140 -325 0
97 -163 -381 0
-275 50 -158 0
252 -378 -234 0
-362 216 -341 0
-283 -216 -119 0
-290 -365 -259 0
304 -122 -388 0
27 357 324 0
-122 -57 -60 0
73 27 -175 0
90 280 -373 0
-337 -120 3 0
-290 -84 152 0
-367 37 299 0
98 -351 -76 0
-88 256 74 0
375 -201 -386 0
-55 -190 -50 0
-334 71 224 0
-191 -285 400 0
239 -133 357 0
-28 -337 -350 0
-258 112 148 0
384 -162 -352 0
331 -15 304 0
-53 -383 -342 0
-48 -37 373 0
-322 22 -76 0
71 -356 112 0
35 -283 -227 0
124 -119 185 0
279 -174 202 0
-206 -221 305 0
365 -232 -347 0
232 -396 10 0
-247 -334 -303 0
-128 -11 -366 0
-321 -133 352 0
-209 -59 351 0
379 46 -269 0
-359 347 199 0
-271 396 60 0
328 50 -380 0
361 -298 274 0
150 -189 86 0
-310 54 3 0
-262 73 26 0
174 197 70 0
125 -321 97 0
-299 -297 236 0
25 55 99 0
-84 291 -265 0
-89 163 371 0
345 18 -193 0
-54 314 280 0
-21 39 257 0
257 84 -356 0
135 -219 137 0
-57 148 43 0
234 206 39 0
114 -87 262 0
-56 329 187 0
-235 -297 -269 0
376 247 41 0
207 -281 -165 0
42 27 244 0
334 -78 321 0
331 354 -177 0
145 53 35 0
361 154 -138 0
52 -56 -143 0
352 -360 -176 0
361 -185 -376 0
52 8 -3 0
290 359 303 0
186 52 -258 0
315 -367 144 0
221 -101 -202 0
293 -399 358 0
-261 13 51 0
-214 -144 -176 0
400 352 -97 0
-268 -16 -136 0
239 -136 97 0
136 234 314 0
270 -135 -315 0
-243 -396 -143 0
-290 -202 99 0
303 98 163 0
3 -357 302 0
139 252 124 0
-16 -135 -279 0
210 -339 -394 0
-347 187 -220 0
-373 -198 251 0
-188 -114 35 0
-19 161 -260 0
-89 -62 -385 0
36 -139 -24 0
-262 -73 205 0
108 -87 53 0
-246 -298 394 0
-177 -331 128 0
-313 379 7 0
-377 288 -13 0
47 185 221 0
41 -62 37 0
-156 86 -82 0
-139 390 354 0
375 -306 -69 0
276 -199 -38 0
248 -233 -100 0
-41 -216 317 0
201 -43 243 0
-276 -125 375 0
-208 -131 274 0
-364 -259 129 0
388 240 290 0
-379 398 -241 0
-382 302 365 0
-329 -183 -294 0
95 -16 47 0
63 348 255 0
-7 -105 364 0
135 218 398 0